翻訳と辞書 |
temporal logic An extension of predicate calculus which includes notation for arguing about *when* statements are true. Time is discrete and extends indefinitely into the future. Three prefix operators, represented by a circle, square and diamond mean "is true at the next time instant", "is true from now on" and "is eventually true". x U y means x is true until y is true. x P y means x precedes y. There are two types of formula: "state formulae" about things true at one point in time, and "path formulae" about things true for a sequence of steps. An example of a path formula is "x U y", and example of a state formula is "next x" or a simple atomic formula such at "waiting". "true until" in this context means that a state formula holds at every point in time up to a point when another formula holds. "x U y" is the "strong until" and implies that there is a time when y is true. "x W y" is the "weak until" in which it is not necessary that y holds eventually. There are two types of te
スポンサード リンク
翻訳と辞書 : 翻訳のためのインターネットリソース |
Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.
|
|